Nuprl Definition : monoid_hom
13,42
postcript
pdf
MonHom(
M1
,
M2
) == {
f
:|
M1
|
|
M2
|| IsMonHom{
M1
,
M2
}(
f
)}
latex
Up
groups
1
Wellformedness Lemmas
monoid
hom
wf
Definitions
|
g
|
,
IsMonHom{
M1
,
M2
}(
f
)
origin
|M2|| IsMonHom{M1,M2}(f)} |M2|| IsMonHom{M1,M2}(f)}